$\forall$$A$, $C$:Type, $B$:($A$$\rightarrow$Type), $x$:$a$:$A$ fp$\rightarrow$ $B$($a$), $y$:$C$, $f$:($C$$\rightarrow$($a$:$A$$\rightarrow$$B$($a$)$\rightarrow$$C$)).
\\[0ex]fpf{-}accum($z$,$a$,$v$.$f$($z$,$a$,$v$);$y$;$x$) $\in$ $C$